It is well-documented that configuration errors cause a large percentage of network downtime and vulnerabilities. Every network component has a finite number of configuration variables (or parameters or knobs) that need to be set to definite values to satisfy end-to-end requirements on security and functionality. Today, a human has to compute the detailed settings of all configuration variables. Since the conceptual gap between requirements and configuration is very large, a large number of configuration errors are made. It is analogous to the situation where compilers for high-level languages are not available and algorithms have to be implemented in assembly language.
The present invention for repairing configuration errors leverages weighted MaxSAT solvers for a Satisfiability Modulo Theories (SMT) language consisting of Equality of Uninterpreted Functions, arithmetic constraints and bit vector constraints. This language is expressive enough for specifying realistic network constraints. A good weighted MaxSAT solver for this SMT language is Yices. The Yices SMT Solver (Yices) is described by B. Dutertre and L. de Moura, The Yices SMT Solver. Tool paper, available online from yices.csl.sri.com/tool-paper.pdf.
The SMT paradigm can be seen as a generalization of classic (propositional) satisfiability. An input to an SMT solver is a quantifier-free formula with various interpreted and uninterpreted function and predicate symbols. Some SMT solvers accept quantified sentences, but the quantifier-free formula are typically removed (expanded away) in these SMT solvers by using various heuristics. The interpreted atoms of the formula come from various background theories, such as linear (integer and real) arithmetic, inductive data types (free algebras, scalar and recursive), uninterpreted functions with equality, the theory of lists, extensional arrays, fixed-size bit vectors, etc. The satisfiability of an input formula p is determined by these background theories, along of course with the Boolean structure of p. An SMT solver will not only determine whether p is satisfiable; if it is, it will also provide appropriate satisfying values for the free variables and/or constants that occur in p. Some SMT solvers also have very useful—albeit more expensive—facilities for computing unsat cores, and for solving weighted Max-SAT problems.
The weighted Max-SAT problem is a variation of the classic satisfiability problem that can model many optimization problems. The difference from the classical setting is that each clause has a unique positive weight associated with it. The task is to find a satisfying assignment for the input formula that maximizes the total weight, i.e., the sum of the weights of the clauses that are satisfied by the assignment. The Max-SAT problem by itself, without weights, is used to maximize the number of satisfied clauses. This can be seen as a special case of the weighted Max-SAT problem, in which every clause is given a weight of 1. Both the weighted and the non-weighted versions of Max-SAT problem are NP-hard. Polynomial-time approximation algorithms are known within a worst-case ratio of 0.785. Yices solvers can solve weighted Max-SAT formulations of SMT problems. Any SMT formula can be asserted with a positive weight, using the command assert+ instead of assert. An infinite weight can be given to an assertion p, effectively ruling out any solutions that falsify p.